n:. nth_tl(n;[]) ~ [] 

latex

Definitions	x:A. B(x), nth_tl(n;as), t  T, Y, if b then t else f fi , i z j, b, i <z j, tt, ff, P  Q, i  j , A  B, A, False, P  Q, , P & Q, P  Q, T, True, tl(l), , , Unit,
Lemmas	nat wf, nat properties, ge wf, le int wf, bool wf, iff transitivity, assert wf, le wf, eqtt to assert, assert of le int, lt int wf, bnot wf, eqff to assert, squash wf, true wf, bnot of le int, assert of lt int